FDL - Nuprl Lemma : fifo-FIFO

Nuprl Lemma : fifo-FIFO

es:ES, ff:FIFO.
for clients ff.C sends FIFO
forfrom j to i via (ff.S[j,i],ff.Codes)
forreceives at i via (ff.R[i],ff.Decodes)

Definitions x:A. B(x), ff.Codes, ff.Decodes, ff.C, ff.S, ff.R, ff.T, let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), t T, FIFO

Lemmas FIFO wf, event system wf

Definitions	x:A. B(x), ff.Codes, ff.Decodes, ff.C, ff.S, ff.R, ff.T, let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), t T, FIFO
Lemmas	FIFO wf, event system wf